Print concrete override precondition failures #416

langston-barrett · 2019-04-22T17:51:47Z

Progress on #414.

Here's what the message looks like now:

  No override specification applies for SHA256_Init.
  The following overrides had some preconditions  that failed concretely:
  
  - Name: SHA256_Init
    Location: /build/fizz-hkdf/main.saw:127:19
    Argument types: 
      %struct.SHA256state_st*
    Return type: i32
    * global initializer equality precondition for global sha256_md
      in _SAW_verify_prestate at /build/fizz-hkdf/main.saw:127:19
    * global initializer equality precondition for global allow_customize
      in _SAW_verify_prestate at /build/fizz-hkdf/main.saw:127:19
  in overrideBranches at /build/fizz-hkdf/main.saw:190:1

re: the redundancy in the line numbers, see #415

langston-barrett · 2019-04-22T21:28:04Z

The error messages now include the expected and actual values. These are a little more unwieldy than I'd like...

This should be redone with unsat cores, but that will be a bit more complicated. For now, fixes GaloisInc#414.

The user will still be wondering what happened.

atomb · 2019-05-14T16:18:09Z

Do you have an example of unwieldy values? I'm inclined to merge this regardless, as it's probably more useful than what we currently have.

langston-barrett · 2019-05-14T22:47:08Z

Here's another example. To get an unwieldy message, you can change the global to a big struct. I'll do that in a minute and post the result here:

/*
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; clang_7" --run "clang -O0 -emit-llvm -c *.c"
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; llvm_7" --run "llvm-dis *.bc"
*/

int z = 4;

int f(int x) {
  return x + x;
}

int g(int x) {
  z = 3;
  return f(f(x));
}

int main() {
  return g(5);
}

m <- llvm_load_module "test.bc";

let init_global name = do {
  crucible_points_to (crucible_global name) (crucible_global_initializer name);
};

let f_spec = do {
  init_global "z";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 2 * x : [32] }});
};

let g_spec = do {
  init_global "z";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 4 * x : [32] }});
};

f_spec <- crucible_llvm_verify m "f" [] false f_spec z3;
crucible_llvm_verify m "g" [f_spec] false g_spec z3;

Loading file "/home/siddharthist/code/tmp/test.saw"
Proof succeeded! f
Registering override for `f`
  variant `f`
"crucible_llvm_verify" (/home/siddharthist/code/tmp/test.saw:22:1-22:21):
Symbolic execution failed.
Abort due to false assumption:
  No override specification applies for f.
  The following overrides had some preconditions that failed concretely:
  - Name: f
    Location: /home/siddharthist/code/tmp/test.saw:21:11
    Argument types: 
      i32
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(z)
      Actual value: 
      literal integer: unsigned value = 3, signed value = 3, width = 32
      in _SAW_verify_prestate at /home/siddharthist/code/tmp/test.saw:21:11
  in overrideBranches at /home/siddharthist/code/tmp/test.saw:22:1
Stack frame
  Allocations:
    StackAlloc 5 0x4:[64] Mutable "internal"
  Writes:
    *(4, 0x0:[64]) := 0x3:[32]
    *(5, 0x0:[64]) := c@8:bv
Base memory
  Allocations:
    GlobalAlloc 4 0x4:[64] Mutable z
    GlobalAlloc 3 0x0:[64] Immutable main
    GlobalAlloc 2 0x0:[64] Immutable g
    GlobalAlloc 1 0x0:[64] Immutable f
  Writes:
    *(4, 0x0:[64]) := 0x4:[32]

langston-barrett · 2019-05-14T22:53:43Z

If we change the global in the above example to be a struct, we get something like the following. Extrapolating to larger structs (e.g. those generated by clang++), you can see where the message might be a bit awkward.

struct foo {
  int u;
  long w;
  char o;
} foo;

Loading file "/home/siddharthist/code/tmp/test.saw"
Proof succeeded! f
Registering override for `f`
  variant `f`
"crucible_llvm_verify" (/home/siddharthist/code/tmp/test.saw:22:1-22:21):
Symbolic execution failed.
Abort due to false assumption:
  No override specification applies for f.
  The following overrides had some preconditions that failed concretely:
  - Name: f
    Location: /home/siddharthist/code/tmp/test.saw:21:11
    Argument types: 
      i32
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(z)
      Actual value: 
      {literal integer: unsigned value = 12, signed value = 12, width = 32
      ;literal integer: unsigned value = 32, signed value = 32, width = 64
      ;literal integer: unsigned value = 8, signed value = 8, width = 8}
      in _SAW_verify_prestate at /home/siddharthist/code/tmp/test.saw:21:11
  in overrideBranches at /home/siddharthist/code/tmp/test.saw:22:1
Stack frame
  Allocations:
    StackAlloc 6 0x4:[64] Mutable "internal"
  Writes:
    *(4, 0x0:[64]) := 0xc:[32]
    *(6, 0x0:[64]) := c@8:bv
Base memory
  Allocations:
    GlobalAlloc 5 0x18:[64] Mutable foo
    GlobalAlloc 4 0x18:[64] Mutable z
    GlobalAlloc 3 0x0:[64] Immutable main
    GlobalAlloc 2 0x0:[64] Immutable g
    GlobalAlloc 1 0x0:[64] Immutable f
  Writes:
    *(4, 0x0:[64]) := {base+0 = 0x22:[32]
                      ,base+8 = 0x20:[64]
                      ,base+16 = 0x8:[8]}

langston-barrett · 2019-05-22T01:08:54Z

@atomb Here's a better example of the unwieldy values:

  No override specification applies for EVP_DigestInit_ex.
  The following overrides had some preconditions that failed concretely:
  - Name: EVP_DigestInit_ex
    Location: /build/fizz-hkdf/digest.saw:149:3
    Argument types: 
      %struct.env_md_ctx_st*
      %struct.env_md_st*
      %struct.engine_st*
    Return type: i32
    * Equality precondition
      Expected value: 
      global_initializer(sha256_md)
      Actual value: 
      {literal integer: unsigned value = 672, signed value =  672, width = 32
      ;literal integer: unsigned value = 668, signed value =  668, width = 32
      ;literal integer: unsigned value = 32, signed value =  32, width = 32
      ;literal integer: unsigned value = 12, signed value =  12, width = 64
      ;concrete pointer: allocation = 512, offset = 0
      ;concrete pointer: allocation = 552, offset = 0
      ;concrete pointer: allocation = 510, offset = 0
      ;<zero : bitvectorType 8>
      ;<zero : bitvectorType 8>
      ;concrete pointer: allocation = 44, offset = 0
      ;concrete pointer: allocation = 45, offset = 0
      ;[literal integer: unsigned value = 6, signed value =  6, width = 32
       ,literal integer: unsigned value = 19, signed value =  19, width = 32
       ,<zero : bitvectorType 4>
       ,<zero : bitvectorType 4>
       ,<zero : bitvectorType 4>]
      ;literal integer: unsigned value = 64, signed value =  64, width = 32
      ;literal integer: unsigned value = 120, signed value =  120, width = 32
      ;<zero : bitvectorType 8>}
      in _SAW_verify_prestate at /build/fizz-hkdf/digest.saw:149:3

langston-barrett added 8 commits April 22, 2019 10:50

[WIP] use labeled predicates

4fecf3d

Print concretely failing override preconditions

cb3cf32

Prettier printing of override matching failure

dec81cd

More specific error messages for preconditions involving globals

66af2c2

Update Crucible submodule (for What4.LabeledPred)

f123d08

Update Crucible submodule: Pretty instance for LLVMVal

4395c17

Show both expected and actual values on equality preconditions

ec8220c

Add some newlines (the actual value may be a large, complex struct)

12a1190

langston-barrett added 2 commits April 22, 2019 16:34

Show symbolically failing override preconditions when possible

66c9fbc

This should be redone with unsat cores, but that will be a bit more complicated. For now, fixes GaloisInc#414.

Add a message when no preconditions symbolically _or_ concretely fail

97ce94c

The user will still be wondering what happened.

langston-barrett added the topics: error-messages Issues involving the messages SAW produces on error label Apr 23, 2019

langston-barrett requested a review from brianhuffman April 24, 2019 22:52

atomb added this to the 0.3 milestone May 14, 2019

langston-barrett added 4 commits May 14, 2019 13:57

Merge remote-tracking branch 'upstream/master' into override-matching

40b63dc

fix merge conflict

f0ec300

Don't print symbolic override matching failures

a09ad89

fix logging bug: null -> not null

fe054b4

Allow the user to see all overrides with --sim-verbose=3

e7c8b89

langston-barrett merged commit 515d433 into GaloisInc:master May 14, 2019

langston-barrett deleted the override-matching branch May 14, 2019 23:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Print concrete override precondition failures #416

Print concrete override precondition failures #416

langston-barrett commented Apr 22, 2019 •

edited

Loading

langston-barrett commented Apr 22, 2019

atomb commented May 14, 2019

langston-barrett commented May 14, 2019

langston-barrett commented May 14, 2019

langston-barrett commented May 22, 2019

Print concrete override precondition failures #416

Print concrete override precondition failures #416

Conversation

langston-barrett commented Apr 22, 2019 • edited Loading

langston-barrett commented Apr 22, 2019

atomb commented May 14, 2019

langston-barrett commented May 14, 2019

langston-barrett commented May 14, 2019

langston-barrett commented May 22, 2019

langston-barrett commented Apr 22, 2019 •

edited

Loading